nLab size issues

Overview

There are various ways to deal with size issues in the foundations of mathematics. All of them involve the notion of universe in one way or another.

• In set theory, one usually either uses Grothendieck universes, or some internal model of set theory or class theory, whether well-pointed Heyting categories, well-pointed division allegories, sets with extensional well-founded transitive relations, categories with class structure, et cetera.

• In class theory, the notion of universe is already in the theory via the universal class, which is by definition a class universe.

• In dependent type theory, one uses univalent Russell universes or Tarski universes, which are basically internal models of dependent type theory.

In any case, given a universe $U$, we say that a collection is $U$-small if it is in $U$, a collection is $U$-large if it is not in $U$, any subcollection of $U$ is a class, and a subcollection of $U$ is a proper class if it is not a singleton subcollection of $U$.

See also

• set, proper class, Grothendieck universe
• small category, essentially small category, large category
• Set, Cat, category of all sets
• small presheaf, accessible category, presentable category